<html>
<head><meta charset="utf-8"><title>Access to MIR from third-party tools · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html">Access to MIR from third-party tools</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="238661186"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238661186" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Tomb <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238661186">(May 13 2021 at 18:33)</a>:</h4>
<p>I'm curious to find out the level of interest among verification tool developers for some sort of standardized way to access MIR from external tools (as opposed to doing so by using the compiler as a library directly from the verification tool). We've been developing a Rust verifier (one instance of <a href="https://crux.galois.com">Crux</a>) by reusing a bunch of verification infrastructure written in Haskell. Because of this, it's difficult to write the verification tool itself in Rust. Our solution is to write a Rust compiler wrapper that serializes MIR (to JSON) and then read that serialized data from the Haskell portion of the tool. However, it seems to me that if anyone else is also doing this we might want to standardize on a format and a tool for generating that format. Would anyone else find this useful?</p>



<a name="238661547"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238661547" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Tomb <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238661547">(May 13 2021 at 18:35)</a>:</h4>
<p>From what I understand, the compiler already serializes MIR for its own use, and that the format just isn't documented (partly because they want to maintain flexibility to change it, IIUC). A solution to this problem _could_ be to work with the compiler team to document that format and perhaps place a little more structure (including version tags, perhaps) on changes to the format.</p>



<a name="238661679"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238661679" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Tomb <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238661679">(May 13 2021 at 18:36)</a>:</h4>
<p>Another aspect we've considered is whether incremental access to MIR (where a client could ask for the MIR representation of one function at a time, for example) could be possible, perhaps through rust-analyzer.</p>



<a name="238677838"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238677838" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238677838">(May 13 2021 at 20:41)</a>:</h4>
<p><a href="https://github.com/rust-lang/lang-team/blob/master/design-meeting-minutes/2021-02-17-Increasing-Trust-in-Rust-Compiler.md">https://github.com/rust-lang/lang-team/blob/master/design-meeting-minutes/2021-02-17-Increasing-Trust-in-Rust-Compiler.md</a> may be of interest.</p>



<a name="238677989"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238677989" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238677989">(May 13 2021 at 20:42)</a>:</h4>
<p>Rust-analyzer doesn't do any codegen and as such doesn't have anything similar to MIR.</p>



<a name="238678120"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238678120" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238678120">(May 13 2021 at 20:43)</a>:</h4>
<p>Note that MIR in itself is useless. You need the whole typesystem to interpret it.</p>



<a name="238690240"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238690240" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Tomb <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238690240">(May 13 2021 at 22:25)</a>:</h4>
<p>Oh, that's very interesting! Thanks for pointing it out. Lots of encouraging signs in those notes. I agree that semver compatibility is plenty.</p>



<a name="238690368"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238690368" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Tomb <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238690368">(May 13 2021 at 22:26)</a>:</h4>
<p>And, yes, to the point about the type system: our serialization code also includes all the types (at least those that are used). A standardized representation of MIR would probably only be useful if it did, too.</p>



<a name="238791874"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238791874" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238791874">(May 14 2021 at 16:21)</a>:</h4>
<p><span class="user-mention" data-user-id="209572">@Aaron Tomb</span> I've been thinking about the idea of extacting the logic from miri that gives access to MIR</p>



<a name="238791913"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238791913" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238791913">(May 14 2021 at 16:21)</a>:</h4>
<p>I think there would be room for a great "building block" project that lots of verifiers can use</p>



<a name="238791968"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238791968" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238791968">(May 14 2021 at 16:21)</a>:</h4>
<p>I've not dug deeply into miri (cc <span class="user-mention" data-user-id="124288">@oli</span> and <span class="user-mention" data-user-id="120791">@RalfJ</span> though) to know what this would look like, though</p>



<a name="238792996"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238792996" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238792996">(May 14 2021 at 16:27)</a>:</h4>
<p>Miri just uses <code>tcx.instance_mir</code> to access the MIR for an <code>Instance</code>. This is the same query that is used for codegen.</p>



<a name="238794215"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238794215" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Tomb <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238794215">(May 14 2021 at 16:36)</a>:</h4>
<p>That's great to hear, <span class="user-mention" data-user-id="116009">@nikomatsakis</span>. Is your thought that that would be primarily available as a library, for Rust clients, or might it include serialization (in a specified format), for more portable access to that data? I imagine one path could be to start with a library, to clarify exactly what information is needed, and follow up with serialization after that, once the library is stable.</p>



<a name="238814043"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238814043" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238814043">(May 14 2021 at 19:02)</a>:</h4>
<p><span class="user-mention" data-user-id="209572">@Aaron Tomb</span> my thought is that it would be interfacing live with the compiler's query system, but I think we should create designated APIs. I don't think we should expose precisely the same MIR that the compiler uses.</p>



<a name="238814073"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238814073" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238814073">(May 14 2021 at 19:02)</a>:</h4>
<p>I would expect we can create a more stable version that changes less and has a few less details, and a layer to translate</p>



<a name="238814091"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238814091" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238814091">(May 14 2021 at 19:02)</a>:</h4>
<p>so that compiler refactorings don't necessarily affect external clients (and we can version and detect it when they do)</p>



<a name="238814149"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238814149" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238814149">(May 14 2021 at 19:03)</a>:</h4>
<p>i think <span class="user-mention" data-user-id="133247">@bjorn3</span> it's not just that, it's also about accessing the MIR for library code and some other bits of knowledge.</p>



<a name="238817594"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238817594" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238817594">(May 14 2021 at 19:31)</a>:</h4>
<p>Miri uses <code>-Zalways-encode-mir</code> for library MIR.</p>



<a name="238818373"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238818373" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238818373">(May 14 2021 at 19:36)</a>:</h4>
<p>I think a more stable MIR would require monomorphization. That way we can for example include the layout for all types and not require normalization of types.</p>



<a name="238821093"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238821093" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238821093">(May 14 2021 at 19:57)</a>:</h4>
<p>That could be one option, to expose mir only post monomorphization in the default interface, but I don't think it's a very good one. I'd be ok with "working our way towards stable" =)</p>



<a name="238821169"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238821169" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238821169">(May 14 2021 at 19:57)</a>:</h4>
<p>as for what miri does, I'm not sure, I just know that some effort has been put into making the workflow relatively smooth, and that effort is often replicated (but not as well)</p>



<a name="238837643"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238837643" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Tomb <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238837643">(May 14 2021 at 22:24)</a>:</h4>
<p>I like the approach of working with the query system, as it means that some sort of server that could produce MIR for individual functions on demand could work. (Our current system serializes an entire crate, which takes a while and generates huge files.) And having a slightly different MIR for external consumption also sounds good to me.</p>



<a name="238837849"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238837849" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Tomb <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238837849">(May 14 2021 at 22:27)</a>:</h4>
<p>Also, FWIW, our MIR -&gt; JSON translator works post monomorphization to simplify the language the verifier needs to work with, so a system that supported only that would be exactly what we need (though perhaps not what everyone would need). Am I right in thinking that monomorphized MIR is a strict subset of MIR, and that therefore starting with support for monomorphized MIR and later adding polymorphic MIR would be backward compatible? Maybe that's what you mean by "working towards stable"?</p>



<a name="238839960"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238839960" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238839960">(May 14 2021 at 22:52)</a>:</h4>
<p>I think many folks are working with monomorphized mIR yes</p>



<a name="238888389"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238888389" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238888389">(May 15 2021 at 10:49)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools/near/238821169">said</a>:</p>
<blockquote>
<p>as for what miri does, I'm not sure, I just know that some effort has been put into making the workflow relatively smooth, and that effort is often replicated (but not as well)</p>
</blockquote>
<p>basically it does <code>-Zalways-encode-mir</code>, but then a lot of work is required to ensure that <em>everything</em> (including the standard library) is built with that flag. This work is almost entirely done by cargo-miri, which is a separate binary (that doesnt link against the compiler or use any nightly features itself). cargo-miri uses xargo, cargo and a ton of hacks to invoke the core Miri driver in just the right way so that in the end we end up with having MIR available for everything -- and we can do that for arbitrary <code>--target</code> without having any part of that target toolchain installed.</p>



<a name="238971336"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238971336" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238971336">(May 16 2021 at 11:49)</a>:</h4>
<p>I’d definitely be interested in improved and more stable queries to interact with MIR but I’m not certain that serialized access is all that interesting at least for my use case.</p>



<a name="238971431"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238971431" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238971431">(May 16 2021 at 11:50)</a>:</h4>
<p>￼I find myself needing a lot more than just the syntax of mir programs, it’s quite useful to query for various type information like which traits are available on a specific type parameter</p>



<a name="238971454"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/238971454" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#238971454">(May 16 2021 at 11:51)</a>:</h4>
<p>Additionally, in my case I’m working on polymorphic MIR</p>



<a name="239046431"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239046431" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Vytautas Astrauskas [he/him] <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239046431">(May 17 2021 at 07:43)</a>:</h4>
<p><span class="user-mention silent" data-user-id="312719">Xavier Denis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools/near/238971454">said</a>:</p>
<blockquote>
<p>Additionally, in my case I’m working on polymorphic MIR</p>
</blockquote>
<p>Same with Prusti.</p>



<a name="239125304"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239125304" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239125304">(May 17 2021 at 17:03)</a>:</h4>
<p>I would expect to expose polymorphic MIR</p>



<a name="239125345"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239125345" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239125345">(May 17 2021 at 17:03)</a>:</h4>
<p>one thing that is relevant is that the traits WG is working towards having a separate crate (shared by rustc, rust-analyzer, and chalk) to encode the rust type system</p>



<a name="239648659"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239648659" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Tomb <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239648659">(May 20 2021 at 19:47)</a>:</h4>
<p>On a more logistical note, has there been any progress on determining what group would continue the conversation from the "Increasing trust in rust compiler" meeting from 02/17? I'd love a chance to get involved.</p>



<a name="239667184"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239667184" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239667184">(May 20 2021 at 22:14)</a>:</h4>
<p>There's been some discussion but not a full proposal. I've been talking some to <span class="user-mention" data-user-id="228996">@Sabree Blackmon</span> and <span class="user-mention" data-user-id="120791">@RalfJ</span> about it. I'd like to see a lang team project proposal with a fairly clear scope, targeted at "defining an operational semantics for MIR", I think.</p>



<a name="239667256"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239667256" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239667256">(May 20 2021 at 22:14)</a>:</h4>
<p>That said, I'm not even sure if it's necessary to go that far. Like maybe we should just create a space for people to start poking at something and see where it goes.</p>



<a name="239667281"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239667281" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239667281">(May 20 2021 at 22:14)</a>:</h4>
<p>I would like to have regular check-ins with the lang team, so calling it a project makes sense to me.</p>



<a name="239667319"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239667319" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239667319">(May 20 2021 at 22:15)</a>:</h4>
<p>It's going to take some organizational effort though.</p>



<a name="239667474"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239667474" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239667474">(May 20 2021 at 22:16)</a>:</h4>
<p>Another idea I was kicking around with <span class="user-mention" data-user-id="372005">@Nathan Chong</span>  was kind of a "formal semantics office hours", where we would try to just have a time for folks who are building verifiers etc to come and ask questions with various people from compiler/lang teams about interesting bits of the semantics.</p>



<a name="239766024"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239766024" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239766024">(May 21 2021 at 15:09)</a>:</h4>
<p>I like the idea of having some kind of office hours to ask questions or, perhaps, to discuss common issues!</p>
<p>(I don't happen to have any questions about MIR though since I am working at the LLVM-IR level. But I expect that we have other topics we might want to discuss. eg the most recent I came across was "how do people want to write axioms that trait methods are supposed to obey?")</p>
<p>How would the office hours work? Do we just all turn up here at 4pm on a Friday afternoon and ask questions?</p>



<a name="239767672"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239767672" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239767672">(May 21 2021 at 15:20)</a>:</h4>
<p><span class="user-mention" data-user-id="336739">@Alastair Reid</span> I was imagining that we might submit questions in advance, but yes that's the rough idea</p>



<a name="239767694"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239767694" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239767694">(May 21 2021 at 15:20)</a>:</h4>
<p>submitting in advance might be a bit overkill</p>



<a name="239767707"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239767707" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239767707">(May 21 2021 at 15:20)</a>:</h4>
<p>otoh it gives time to do a bit of prep</p>



<a name="239767750"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239767750" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239767750">(May 21 2021 at 15:21)</a>:</h4>
<p>I would like it if we recorded the outcomes a bit</p>



<a name="239767779"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239767779" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239767779">(May 21 2021 at 15:21)</a>:</h4>
<p>it seems like a waste to just talk</p>



<a name="239769768"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239769768" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Chong <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239769768">(May 21 2021 at 15:33)</a>:</h4>
<p>I love the idea of a semantics office hours and would be very happy to drive the organization/setup, if appropriate. Maybe questions could be posted ahead of time so there's context and grouping up of related topics, but I think simply having the forum on a regular cadence would enable us to work this out.</p>



<a name="239770269"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239770269" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Chong <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239770269">(May 21 2021 at 15:37)</a>:</h4>
<p>And yes, I think an aim should be for each meaty question to reach a fixed-point where we can write up findings and push them into the nomicon/other docs</p>



<a name="239787722"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239787722" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239787722">(May 21 2021 at 17:42)</a>:</h4>
<p>I think weekly would be too frequent</p>



<a name="239787752"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239787752" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239787752">(May 21 2021 at 17:42)</a>:</h4>
<p>maybe every 2 or 4 weeks?</p>



<a name="239787760"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239787760" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239787760">(May 21 2021 at 17:42)</a>:</h4>
<p>I'd be good to just try it for a while and see how it goes</p>



<a name="239787797"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239787797" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239787797">(May 21 2021 at 17:42)</a>:</h4>
<p>I would ask <span class="user-mention" data-user-id="372005">@Nathan Chong</span> that maybe you can author blog posts we can post on <a href="https://blog.rust-lang.org/inside-rust/">the Inside Rust blog</a> summarizing the questions and thoughts we had</p>



<a name="239787831"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239787831" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239787831">(May 21 2021 at 17:43)</a>:</h4>
<p>the nomicon etc would be good too, but I imagine that may take longer sometimes</p>



<a name="239787884"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239787884" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239787884">(May 21 2021 at 17:43)</a>:</h4>
<p>I have to be a bit careful because I'm trying to carve out more time for coding and chalk :)</p>



<a name="239811532"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239811532" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Nathan Chong <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239811532">(May 21 2021 at 20:52)</a>:</h4>
<p>Sure, I'd be happy to take point on writing-up summaries! Let's do this :)</p>



<a name="239972717"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239972717" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239972717">(May 23 2021 at 19:27)</a>:</h4>
<p>I love the idea of office hours, it would also help if there is someone with knowledge of compiler internals as often building against mir means digging into them (for now)</p>



<a name="239972740"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/239972740" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#239972740">(May 23 2021 at 19:27)</a>:</h4>
<p>I think at this point I have a decent amount of query expertise but I’m not always certain if I’m taking the direct or intended route to my objectices</p>



<a name="240486860"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/240486860" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Aaron Tomb <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#240486860">(May 27 2021 at 15:38)</a>:</h4>
<p>I also love the idea of having office hours.</p>



<a name="240617141"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/240617141" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#240617141">(May 28 2021 at 15:06)</a>:</h4>
<p>So <span class="user-mention" data-user-id="372005">@Nathan Chong</span> and I were <a href="https://hackmd.io/2sIKMuUGQY2jug9GdCm-WQ">collecting ideas here</a></p>



<a name="240617166"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/240617166" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#240617166">(May 28 2021 at 15:06)</a>:</h4>
<p>it'd be helpful for people to note the kinds of questions they have or expect to have</p>



<a name="240924576"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/240924576" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hilmar Gústafsson <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#240924576">(Jun 01 2021 at 10:57)</a>:</h4>
<p><span class="user-mention silent" data-user-id="116009">nikomatsakis</span> <a href="#narrow/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools/near/239667184">said</a>:</p>
<blockquote>
<p>There's been some discussion but not a full proposal. I've been talking some to <span class="user-mention silent" data-user-id="228996">Sabree Blackmon</span> and <span class="user-mention silent" data-user-id="120791">RalfJ</span> about it. I'd like to see a lang team project proposal with a fairly clear scope, targeted at "defining an operational semantics for MIR", I think.</p>
</blockquote>
<p>I've been a part of an effort (master's thesis in a group of two) to create a formal semantics for a subset of MIR - only what is necessary to define a taint analysis . I would love to hear some more about the ideas, and how we could help.</p>



<a name="240926937"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/240926937" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hilmar Gústafsson <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#240926937">(Jun 01 2021 at 11:22)</a>:</h4>
<p>We would also be interested to know if you are aware of any other efforts to define a formal semantics for MIR. We are not aware of any, and would like to say that we are making a novel effort in that regard. We are also more than happy to share our current progress. :)</p>



<a name="241119356"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Access%20to%20MIR%20from%20third-party%20tools/near/241119356" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Andrea Lattuada <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Access.20to.20MIR.20from.20third-party.20tools.html#241119356">(Jun 02 2021 at 08:30)</a>:</h4>
<p>Hi folks, as someone involved in (yet another) rust verification project, I think office hours could be quite useful. I've added one question we are trying to resolve to the hackmd: let me know in case this is _not_ the kind of semantics questions you're planning to address. Thank you!</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>